Nuprl Lemma : ring_p_wf
13,42
postcript
pdf
T
:Type,
pl
:(
T
T
T
),
zero
:
T
,
neg
:(
T
T
),
tm
:(
T
T
T
),
one
:
T
.
IsRing(
T
;
pl
;
zero
;
neg
;
tm
;
one
)
latex
Up
rings
1
Definitions of Statement
IsRing(
T
;
plus
;
zero
;
neg
;
times
;
one
)
Definitions
P
&
Q
,
IsRing(
T
;
plus
;
zero
;
neg
;
times
;
one
)
,
,
t
T
,
x
:
A
.
B
(
x
)
Lemmas
bilinear
wf
,
monoid
p
wf
,
group
p
wf
origin
T:Type, pl:(T
TT), zero:T, neg:(TT), tm:(TTT), one:T.
T:Type, pl:(TTT), zero:T, neg:(TT), tm:(TTT), one:T.
Tx:A. B(x)